nLab partial combinatory algebra

Redirected from "realizability tripos".
Contents

Contents

Idea

A partial combinatory algebra is a generalization of a model of the untyped lambda calculus allowing for application to be only partially defined. It is often expressed as an algebraic abstraction of combinatory logic.

Definition

The following definitions are taken from Hofstra.

A partial applicative structure is a set equipped with a partial binary operation

m:A×AAm \colon A \times A \to A

An application of mm is indicated by juxtaposition: aba b denotes m(a,b)m(a, b) if (and only if) m(a,b)m(a, b) is defined, i.e., if (a,b)(a, b) belongs to the domain of mm. Homomorphisms between partial applicative structures A,BA, B are defined to be total functions f:ABf \colon A \to B such that f(ab)=f(a)f(b)f(a b) = f(a)f(b), meaning the right side is defined whenever the left side is. In other words, in the locally posetal bicategory of sets and relations, we have a 2-cell

A×A f×f B×B m m A f B\array{ A \times A & \stackrel{f \times f}{\to} & B \times B \\ m \downarrow & \leq & \downarrow m \\ A & \underset{f}{\to} & B }

By convention, unbracketed juxtapositions are associated to the left, so that for example xyzx y z means (xy)z(x y)z.

If AA is a partial applicative structure and Magma(A)\mathbf{Magma}(A) is the free magma on the underlying set of AA, then we have an evident partial function

α:Magma(A)A\alpha \colon \mathbf{Magma}(A) \to A

which evaluates binary words in AA as elements in AA, whenever possible, using the partial applicative structure and induction on the structure of the word.

Definition

A partial applicative structure AA is a partial combinatory algebra (a PCA) if there are elements k,sAk, s \in A such that

  • For all a,bAa, b \in A, kak a and kabk a b are defined and kab=ak a b = a.
  • For all a,bAa, b \in A, sas a and sabs a b are defined and for all cc, (ac)(bc)(a c)(b c) is defined if and only if sabcs a b c is defined, and sabc=(ac)(bc)s a b c = (a c)(b c).

A homomorphism of PCA’s is a homomorphism of the underlying partial applicative structures.

A total combinatory algebra is a PCA AA whose application m:A×AAm \colon A \times A \to A is a total function.

Note that appropriate elements kk, ss are not considered part of the structure (to be preserved under homomorphism) – here one is interested only in the property that such elements exist. Indeed, they need not be uniquely determined within the PCA.

Functional completeness

The definition of PCA given above is traditional but somewhat opaque at first glance. The real point of the definition is that a PCA is the same thing as a partial applicative structure AA that enjoys a functional completeness property, in the following sense.

Let XX be a countably infinite set of “variables”, and let A[X]A[X] denote the magma freely generated from the disjoint sum A+XA + X. Each term tt, i.e., each element tA[X]t \in A[X], has finitely many x iXx_i \in X occurring inside it; these are called the free variables of tt, and we write FV(t)FV(t) for the set of free variables. If FV(t){x 0,x 1,,x n}FV(t) \subseteq \{x_0, x_1, \ldots, x_n\}, then we can think of tt as giving a partially defined function in n+1n+1 variables. That is, we may consider tt as a term of Magma(A+{x 0,,x n})\mathbf{Magma}(A + \{x_0, \ldots, x_n\}), and (partially) define the substitution t[a 0/x 0,,a n/x n]t[a_0/x_0, \ldots, a_n/x_n] where a 0,,a na_0, \ldots, a_n are elements of AA, by evaluating at tt of the composite

Magma(A+{x 0,,x n})Magma(ϕ)Magma(A)αA\mathbf{Magma}(A + \{x_0, \ldots, x_n\}) \stackrel{\mathbf{Magma}(\phi)}{\to} \mathbf{Magma}(A) \stackrel{\alpha}{\to} A

where ϕ(x i)=a i\phi(x_i) = a_i and is elsewhere the identity.

Then, we say AA is functionally complete if every term tA[X]t \in A[X], viewed as a partial operation on AA, is represented by some element in AA. To be precise: for each term tt with FV(t){x 0,,x n}FV(t) \subseteq \{x_0, \ldots, x_n\}, there exists an element aAa \in A such that

  • For all a 0,,a n1Aa_0, \ldots, a_{n-1} \in A, aa 0a n1a a_0 \ldots a_{n-1} is defined;

  • For all a 0,,a nAa_0, \ldots, a_n \in A, t[a 0/x 0,,a n/x n]t[a_0/x_0, \ldots, a_n/x_n] is defined precisely when aa 0a na a_0 \ldots a_n is defined, and these two elements are equal.

For example, if kk, ss are elements which realize AA as a PCA, then kk represents the term t=x 0t = x_0 viewed as belonging to Magma(A+{x 0,x 1})\mathbf{Magma}(A + \{x_0, x_1\}), and ss represents the term (x 0x 2)(x 1x 2)(x_0 x_2)(x_1 x_2) viewed as belonging to Magma(A+{x 0,x 1,x 2)}\mathbf{Magma}(A + \{x_0, x_1, x_2)\}.

Theorem

A partial combinatory algebra is functionally complete.

Proof

The idea is to simulate λ\lambda-abstraction λx.t\lambda x. t, where xXx \in X is a variable and tt is a term, by induction on tt. Indeed, given elements k,sk, s that realize AA as a PCA, put

λx.x skk λx.t kt ifxFV(t) λx.tt s(λx.t)(λx.t)\array{ \lambda x. x & \coloneqq & s k k & \\ \lambda x. t & \coloneqq & k t & if x \notin FV(t) \\ \lambda x. t t' & \coloneqq & s(\lambda x. t)(\lambda x. t') }

One then proves equality of partial functions (λx.t)(a)=t[a/x](\lambda x. t)(a) = t[a/x], by induction on tt.

Hofstra defines a PCA to be a functionally complete partial applicative structure. This is an unbiased definition, in the sense that it does not privilege certain elements kk, ss (or, for that matter, any other system of combinators that provide functional completeness).

Examples of combinators

  1. Let us check that skks k k indeed represents the identity function II. This is trivial: we have, for any aAa \in A, equalities between defined terms

    skka=(ka)(ka)=a.s k k a = (k a)(k a) = a.
  2. Consider the second projection function, corresponding to x 1Magma(A+{x 0,x 1})x_1 \in \mathbf{Magma}(A + \{x_0, x_1\}). Thinking in terms of λ\lambda-terms, this is represented by λx.λy.y=λx.skk=k(skk)\lambda x. \lambda y. y = \lambda x. s k k = k(s k k), or kIk I. In other words, we calculate

    kIab=((kI)a)b=Ib=b.k I a b = ((k I) a) b = I b = b.
  3. Following the proof of functional completeness, we have

    λx.xx=s(λx.x)(λx.x)=sII\lambda x. x x = s(\lambda x. x)(\lambda x. x) = s I I
  4. Finally, consider the classical construction of the fixed-point combinator, Y=λy.(λx.y(xx))(λx.y(xx))Y = \lambda y. (\lambda x. y(x x))(\lambda x. y(x x)). We have firstly

    λx.y(xx)=s(λx.y)(λx.xx)=s(ky)(sII)\lambda x. y(x x) = s(\lambda x. y)(\lambda x. x x) = s(k y)(s I I)

    which means

    Y = λy.(sII)(s(ky)(sII)) = s(λy.sII)(λy.s(ky)(sII)) = s(k(sII))(s(λy.s(ky))(λy.sII)) = s(k(sII))(s(s(ks)k)(k(sII)))\array{ Y & = & \lambda y. (s I I)(s(k y)(s I I)) \\ & = & s(\lambda y. s I I)\big(\lambda y. s(k y)(s I I)\big) \\ & = & s(k (s I I)) \big(s(\lambda y. s(k y))(\lambda y. s I I)\big) \\ & = & s(k (s I I)) \big(s(s(k s)k)(k (s I I))\big) }

Examples of PCAs

  1. (Kleene’s first algebra.) Suppose given a coding of all partial recursive functions of the form k\mathbb{N}^k \to \mathbb{N} (ranging over k=0,1,2,k = 0, 1, 2, \ldots) by elements of \mathbb{N}, and a coding of elements of k\mathbb{N}^k over all kk by elements of \mathbb{N}. Define a partial applicative structure

    ×\mathbb{N} \times \mathbb{N} \to \mathbb{N}

    where pq={p}([q])p q = \{p\}([q]) whenever the right side is defined, where {p}\{p\} is the p thp^{th} partial recursive function and [q][q] is the q thq^{th} tuple. It may be checked that kk and ss, defined extensionally in the obvious way, are partial recursive functions, so we get in this way a PCA.

  2. Suppose we have a cartesian closed category generated by an object XX such that X×XX \times X and X XX^X are retracts of XX. Then elements 1X1 \to X form a PCA, in fact a total combinatory algebra, where the applicative structure is

    X×Xr×1 XX X×XevalXX \times X \stackrel{r \times 1_X}{\to} X^X \times X \stackrel{eval}{\to} X

    for some chosen retraction rr. In other words, models of the untyped lambda calculus give PCA’s.

  3. Kleene's second algebra.

Realizability toposes

From any PCA, a corresponding “realizability tripos” can be constructed, from which, in turn, a corresponding “realizability topos” can be constructed, as outlined in the article on triposes.

A preliminary technical task is to encode pairing and unpairing functions by elements of AA. By this we mean functions p:A×AAp \colon A \times A \to A, l:AAl \colon A \to A, r:AAr \colon A \to A such that for all (a,a)A×A(a, a') \in A \times A, we have (a,a)=(l(p(a,a)),r(p(a,a)))(a, a') = (l(p(a, a')), r(p(a, a'))). One way of doing this is to put

  • p=λx.λy.λz.zxyp = \lambda x. \lambda y. \lambda z. z x y

  • l=λp.p(λx.λy.x)l = \lambda p. p(\lambda x. \lambda y. x)

  • r=λp.p(λx.λy.y)r = \lambda p. p(\lambda x. \lambda y. y)

whereupon we may calculate

paa = λz.zaa l(paa) = (λz.zaa)(λx.λy.x) = (λx.λy.x)aa = (λy.a)a=a\array{ p a a' & = & \lambda z. z a a' \\ l(p a a') & = & (\lambda z. z a a')(\lambda x. \lambda y. x) \\ & = & (\lambda x. \lambda y. x) a a' \\ & = & (\lambda y. a) a' = a }
r(paa) = (λz.zaa)(λx.λy.y) = (λx.λy.y)aa = (λy.y)a=a\array{ r(p a a') & = & (\lambda z. z a a')(\lambda x. \lambda y. y) \\ & = & (\lambda x. \lambda y. y) a a' \\ & = & (\lambda y. y) a' = a' }

That out of the way, let P(A)P(A) be the power set of AA and let XX be a set. Put a preorder structure on P(A) XP(A)^X as follows: given f,gP(A) Xf, g \in P(A)^X, let Hom(f,g)Hom(f, g) be the set of aa in AA such that for all xx in XX and aa' in f(x)f(x), aaa a' is defined (that is, aa is applicable to aa'), and aaa a' is an element of g(x)g(x). We can turn this into a preorder by taking fgf \leq g just in case Hom(f,g)Hom(f, g) is inhabited.

Theorem

The preorder P(A) XP(A)^X has finite products, finite coproducts, and is cartesian closed. In other words, the preorder P(A) XP(A)^X is a Heyting prealgebra.

Proof

An initial object is given by the constant function taking each xx to the empty subset A\emptyset \subseteq A, and a terminal object is given by the constant function taking each xx to the full subset AAA \subseteq A.

Take f,g:XP(A)f, g \colon X \to P(A). For binary products, define

(fg)(x)={paa|af(x)ag(x)}(f \wedge g)(x) = \{p a a' | a \in f(x) \wedge a' \in g(x)\}

Notice that ll realizes fgff \wedge g \leq f (since l(paa)=al (p a a') = a), and similarly rr realizes fggf \wedge g \leq g. Furthermore, suppose given h:XP(A)h \colon X \to P(A), and that tAt \in A realizes hfh \leq f and uAu \in A realizes hgh \leq g. Then

v=λb.p(tb)(ub)v = \lambda b. p (t b)(u b)

realizes hfgh \leq f \wedge g. Thus fgf \wedge g is a product in the preorder.

For binary coproducts, define

(fg)(x)={pla|af(x)}{pra|ag(x)}(f \vee g)(x) = \{p l a | a \in f(x)\} \cup \{p r a' | a' \in g(x)\}

Then plp l realizes ffgf \leq f \vee g and prp r realizes gfgg \leq f \vee g. Furthermore, suppose tt realizes fhf \leq h and uu realizes ghg \leq h. Then

v=λb.l(b)(p(t(rb))(u(rb)))v = \lambda b. l(b)(p(t(r b))(u(r b)))

realizes fghf \vee g \leq h. Indeed, we have

v(pla) = l(pla)(p(t(r(pla)))(u(r(pla)))) = l(p(ta)(ua)) = ta\array{ v(p l a) & = & l(p l a)(p(t(r(p l a)))(u(r(p l a)))) \\ & = & l(p(t a)(u a)) \\ & = & t a }

and similarly v(pra)=uav(p r a') = u a'. In either case, we see v(b)v(b) lives in h(x)h(x) for any b(fg)(x)b \in (f \vee g)(x).

For cartesian closure, define

(fg)(x)={a|af(x)aaaag(x)}(f \Rightarrow g)(x) = \{a' | \forall a \in f(x) a' a \downarrow \wedge a' a \in g(x)\}

where aaa' a \downarrow is standard shorthand for “aaa' a is defined”. Then for any ff and gg, the combinator λb.l(b)r(b)\lambda b. l(b)r(b) realizes (fg)fg(f \Rightarrow g) \wedge f \leq g, and the combinator λb.λa.pab\lambda b. \lambda a. p a b realizes gf(fg)g \leq f \Rightarrow (f \wedge g).

For any function f:XYf \colon X \to Y, it is immediate that

P(A) f:P(A) YP(A) XP(A)^f \colon P(A)^Y \to P(A)^X

is a functor preorder map that preserves Heyting prealgebra structure.

Furthermore, in the case of a projection map f:Z×YYf \colon Z \times Y \to Y, there will be left and right adjoints to P(A) f:P(A) YP(A) Z×Y((P(A) Z) Y)P(A)^f \colon P(A)^Y \to P(A)^{Z \times Y} (\cong (P(A)^Z)^Y), as induced by the union and intersection maps from P(A) ZP(A)^Z to P(A)P(A).

computability

type I computabilitytype II computability
typical domainnatural numbers \mathbb{N}Baire space of infinite sequences 𝔹= \mathbb{B} = \mathbb{N}^{\mathbb{N}}
computable functionspartial recursive functioncomputable function (analysis)
type of computable mathematicsrecursive mathematicscomputable analysis, Type Two Theory of Effectivity
type of realizabilitynumber realizabilityfunction realizability
partial combinatory algebraKleene's first partial combinatory algebraKleene's second partial combinatory algebra

References

  • Pieter J.W. Hofstra, Partial Combinatory Algebras and Realizability Toposes, (web) (pdf)

Lecture notes include

  • Andrej Bauer, section 2 of Realizability as connection between constructive and computable mathematics, in T. Grubba, P. Hertling, H. Tsuiki, and Klaus Weihrauch, (eds.) CCA 2005 - Second International Conference on Computability and Complexity in Analysis, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, , vol. 326-7/2005. FernUniversität Hagen, Germany, 2005, pp. 378–379. (pdf)

Last revised on December 13, 2021 at 21:41:25. See the history of this page for a list of all contributions to it.